A, B:Realizer. A  R-plus(B;A) 

latex

Definitions	ff, tt, P  Q, if b then t else f fi , True, , t  T, let x = a in b(x), R-plus(A;B), x:A. B(x), P & Q, P  Q, Unit, ,
Lemmas	assert of bnot, eqff to assert, iff transitivity, eqtt to assert, R-sub-plus-right, Rnone-implies, not wf, bnot wf, assert wf, R-sub-self, bool wf, Rnone? wf, es realizer wf